(*  OS.FileSys.chDir "d:\\sml"; use "structures.ml";  *)

(*
 * simplistic implementation of the new analysis for polynomial/linear bounds
 * over the "core language".
 *
 * To operate: evaluate Analyse(Cmd) where 
 * Cmd is a command, represented by an element of the datatype Cmd below.
 *
 *  See examples in examples.ml
 *)
 

(*
 * BASIC DEFINITIONS
 *)

(* Expressions and Commands *)
(*
datatype Expr = plus of Expr * Expr | times of Expr * Expr | Var of int;
datatype Cmd = Skip | Asgn of int * Expr | Choice of Cmd * Cmd |
	       Seq  of Cmd * Cmd  | Loop of int * Cmd;
infix plus;
infix times;
*)
(*
 * STRUCTURES for the analysis.
 *)
 
use "../Common/bjkParser.sml";


(* the same "D" is used for both analyses *)
structure D = struct
 abstype t = Dee of int with
 val Zero = Dee 0;
 val One  = Dee 10;
 val One' = Dee 15;
 val Two  = Dee 20;
 val Three= Dee 30;
 fun lub(Dee x, Dee y) = Dee(Int.max(x,y));
 fun sum(a,b) = 
    if (a=Three) orelse (b=Three) then Three
    else if (a=Zero) then b
    else if (b=Zero) then a
    else Two;
 fun prod(a as Dee x, b as Dee y) =
   if (a=Zero) orelse (b=Zero) then Zero else Dee(Int.max(x,y));
 fun eql(Dee x, Dee y) = (x=y);
 fun isOne(v) = (v = One orelse v = One');
 fun toString(v as Dee x) = let val digit = Int.toString(x div 10)
                       in if v=One' then digit ^ "+" else digit end;
 end                       
end;



(************************************************************)
(* sparse matrix implementation (or maybe it's a graph?) *)
structure mat = struct

	 datatype matrix = M of (int*int*D.t) list;
              (* meaning: a SORTED list of entries (i,j,value)
	         the sorting order is (j,i) to keep columns together *)

	 fun lstPrt(M m) = map (fn (i,j,v) => (i,j,D.toString(v))) m;
	 
	 fun prt(m) = 
		let 
			fun prtInternal([]) = ""
			  | prtInternal((i, j, d)::t) = Int.toString(i) ^ "-(" ^ d ^ ")->" ^ Int.toString(j) ^ ", " ^ prtInternal(t);
		in
			prtInternal(lstPrt(m))
		end;
	 
	 fun I(n:int) = M(List.tabulate(n, (fn(i) => (i+1,i+1,D.One))));

	 fun listsame([],[]) = true
	   | listsame(_,[]) = false
	   | listsame([],_) = false
	   | listsame(m1 as (i1,j1,v1)::t1, m2 as (i2,j2,v2)::t2) =
	        (i1,j1)=(i2,j2) andalso D.eql(v1,v2) andalso listsame(t1,t2);

	 fun same(M m1, M m2) = listsame(m1,m2);


	   (* listsqcup merges sorted lists *)
	 fun listsqcup([],m2) = m2
	   | listsqcup(m1,[]) = m1
	   | listsqcup(m1 as (i1,j1,v1)::t1, m2 as (i2,j2,v2)::t2) =
	        if (i1,j1)=(i2,j2) then (i1,j1,D.lub(v1,v2)) :: listsqcup(t1,t2)
	        else if j1<j2 orelse (j1=j2 andalso i1<i2) then
			     (i1,j1,v1) :: listsqcup(t1,m2)
			else (i2,j2,v2) :: listsqcup(m1,t2)

	 fun sortLst [] = []
	   | sortLst [ent] = [ent]
	   | sortLst (e1::(e2::rst)) = listsqcup([e1], sortLst(e2::rst));	 
			
	 fun sqcup(M m1, M m2) = M(listsqcup(sortLst(m1),sortLst(m2)));

	 fun prod(M m1, M m2) =
	    M(foldr 
	        listsqcup 
	        []
	        (map
	          (fn (i1,j1,v) =>  (* multiply one entry from m1 by whole of m2*)
	             foldr (fn ((i2,j2,u), acc) =>
						if j1=i2 then (i1,j2,D.prod(v,u))::acc
						         else acc)
	               []
	               m2
	           )
	          m1 
	         ));

      (* lst2mat sorts its input - inefficiently *)
	   fun lst2mat [] = M([])
		 | lst2mat [ent] = M([ent])
		 | lst2mat (e1::(e2::rst)) = sqcup(M [e1], lst2mat(e2::rst));


(* compute a matrix which is like (I n) except that column j is replaced
   with the provided 'col' *)
fun ins_in_I(n,j,col) =
    M(let val M(Ilist) = I(n)
      in
        foldr
        (fn ((i,jj,v),acc) => (( if jj=j then col else [(i,jj,v)] ) @ acc))
        []
        Ilist
      end);
(*
	  fun star m =
      let fun clos(x) =
      let val next = sqcup(x,prod(x,m)) in if next=x then x else clos(next) end
	   in
	    clos(I(dim m))
	   end
*)
			 
	fun LC(l:int, nonlinear:D.t) (M m) =
          M(listsqcup(m, List.mapPartial
			 (fn (ent as (i,j,v)) => 
				     if j=l andalso i<>l then raise Fail "loop variable modified"
				     else if i=j then
				       if D.eql(v,D.One') then SOME (l,j,nonlinear) 
				  else if D.eql(v,D.Two) then SOME (l,j,D.Three)
                                  else NONE
				  else NONE)
			  m));

(* the r(M) function: extract all pairs of One/One' entries *)
fun ones(M(m)) =
       List.filter (fn (_,_,d) => D.isOne(d)) m;

fun r(m) =
  let 
  val ones' = ones(m)
  in
  foldl 
   (fn ((i,j,d),acc) => 
       acc @
       (List.mapPartial (fn (i',j',d) => 
                 if (i'<i) orelse (i'=i andalso j'<j)
		  then SOME ((i,j),(i',j'))
		  else NONE)
	   ones'))
   [] ones'
  end;

(* classify the variables into "properly bounded" (called SAFE in the paper)
   and the rest.  The Unbounded ones are given first!! *)
fun classify(M m, vars) :(int list)*(int list) = 
     List.partition (fn i => 
               List.exists  (fn (_,j,d) => (j=i andalso D.eql(d,D.Three))) m)
                    (List.tabulate (vars, (fn(i) => i+1)))

end; (* struct mat *)
(************************************************************)


(* DFR - a structure for the SOP method.  Using the "sparse matrix"
 * representation.
 *)

structure sop_bar = struct

 type PosPar = (int * int) * (int * int);
 
 datatype DFR = dfr of mat.matrix * (PosPar list);
 
(*  the identity DFR *)
fun dfrI(n) =
 	let val idMat = mat.I (n)
 	in
       dfr(idMat, mat.r(idMat))
    end;

fun prtR(dfr(_,r)) = 
	let
		fun prtRList([]) = ""
		  | prtRList( ((i,j),(i',j'))::t ) = "(" ^ Int.toString(i) ^ "->" ^ Int.toString(j) ^ ", " ^ Int.toString(i') ^ "->" ^ Int.toString(j') ^ "), " ^ prtRList(t);
	in
		prtRList(r)
	end;
(* functions for sorting/merging R's (represented as sorted PosPar lists *) 

fun lexlt(((a,b),(c,d)):PosPar, ((aa,bb),(cc,dd))) =
  if (b<bb) then true 
   else if (b>bb) then false else if (a<aa) then true
    else if (a>aa) then false else if (d<dd) then true else if (d>dd) then false else (c<cc);

fun merge([],ys) = ys : PosPar list
  | merge(xs,[]) = xs
  | merge(x::xs, y::ys) =
      if lexlt(x,y) then x::merge(xs,  y::ys)
              else if x=y then merge(x::xs, ys) else y::merge(x::xs,  ys);
              
(* sort(already-sorted, yet-not-sorted) *)
fun sort(xs, []) = xs
  | sort(xs, y::ys) = let fun insert [] = [y] 
                            | insert(x::xs) = if lexlt(x,y) then x::insert(xs)
                                                else if x=y then x::xs else y::x::xs
                      in sort(insert(xs), ys) end;

fun filterRDuplicates([] : PosPar list) = []
  | filterRDuplicates((r as ((a,b),(c,d)))::rs : PosPar list) =
		case (List.find (fn(((a',b'),(c',d'))) => (a=a' andalso b=b' andalso c=c' andalso d=d')) rs) of 
					SOME _ => filterRDuplicates(rs)
				  | NONE   => r::filterRDuplicates(rs);

(* remove from r those entries which do not correspond to a 1/1+ *)
fun filterR(r: PosPar list, m: mat.matrix) =
 let
  val ones' = mat.ones(m)
 in
  filterRDuplicates(List.filter (fn ((a,b),(c,d)) =>
                    (List.exists (fn (i,j,_) => (i,j)=(a,b)) ones')
	    andalso (List.exists (fn (i,j,_) => (i,j)=(c,d)) ones') )
		r)
 end;

                      
(* operations on DFRs *)    
fun dfrEmpty(dfr(mat.M([]),[])) = true
  | dfrEmpty(_) = false;

fun dfrsame(dfr(M1,R1),dfr(M2,R2)) =
        mat.same(M1,M2) andalso (R1=R2);
                      
(* product of DFR's *)

(* first, product without handling 'diamonds' *)
fun naiveProd([((a,c),(b,d))],[((e,g),(f,h))]) =
sort ([], 
 (if c=d andalso d=f then [((a,h),(b,h))] else nil)  @
 (if c=d andalso d=e then [((a,g),(b,g))] else nil)  @
 (if c=e andalso d=f then [((a,g),(b,h))] else nil)  @
 (if c=f andalso d=e then [((a,h),(b,g))] else nil)  @
 (if c=e andalso e=f then [((a,g),(a,h))] else nil)  @
 (if d=e andalso e=f then [((b,g),(b,h))] else nil)  
      )
| naiveProd(R1, R2) =
 List.foldr (fn (p:PosPar,Ls) => merge(
        List.foldr (fn ((q:PosPar),Ls) => merge(
				naiveProd([p],[q]),Ls)) [] R2,
        Ls)) [] R1;

(* mine R: splits a result of naiveprod into two lists, one containing the positions
 that have to become 2 because of diamonds, the other is the rest of the list,
 to become the R of the product *)
fun mine([]: PosPar list) = ([],[])
  | mine((h as ((a,c),(b,d)))::t) =
       let val (diamonds, rest) = mine t 
       in
          if (a,c)=(b,d) then ( (a,c,D.Two)::diamonds, rest )
	                 else ( diamonds, h::rest )
       end;

(* another part of product computation:   
   parts of R' created by a 1 in the lhs and a fanout in the rhs. *)    
fun prod1(lhsM:mat.matrix, rhsR:PosPar list) =
  let 
  val ones' = mat.ones(lhsM)
  in
   foldl 
   (fn (((s,j'),(t,j'')),acc) => 
       merge (acc,
       (List.mapPartial (fn (i,j,_) => 
                 if (s=t) andalso (s=j)
		  then SOME ((i,j'),(i,j''))
		  else NONE)
	    ones')))
   [] rhsR
  end 
		
(* the symmetric thing:
   parts of R' created by a 1 in the rhs and a fanin in the rhs. *)    
fun prod2(lhsR:PosPar list, rhsM:mat.matrix) =
  let 
  val ones' = mat.ones(rhsM)
  in
   foldl 
   (fn ((s,t,_),acc) => 
       merge (acc,
       (List.mapPartial (fn ((i,j),(i',j')) => 
                 if (j=j') andalso (j=s)
		  then SOME ((i,t),(i',t))
		  else NONE)
	    lhsR)))
   [] ones'
  end 
  
fun prod(dfr(A,Ra), dfr(B,Rb)) =
  let val p1 = prod1(A,Rb) and p2 = prod2(Ra,B);
      val (d,r) = mine(naiveProd(Ra,Rb));
      val m' = mat.sqcup(mat.prod(A,B), mat.lst2mat(d));
  in
   dfr (m' , filterR(merge(merge(r,p1),p2),m'))
  end;
  
(* join of DFRs *)

fun sqcup(dfr(M1,R1), dfr(M2,R2)) =
 let val M = mat.sqcup(M1,M2);
 in  dfr(M, filterR(merge(R1,R2), M))
 end;
 
(* "loop closure" *)

local
fun fix f x =
   let val x' = f x
   in
      if dfrsame(x,x') then x else fix f x'
   end;
fun loopAux LC (dfr(M,R)) = 
  let val tmpM = LC(M);
      val tmpDFR = dfr(tmpM, filterR(R,tmpM))
  in
      prod(tmpDFR,tmpDFR)
  end;
in
 (*******NB this is without the iteration count ************)
 fun loop(l,vars,nonlinear,MR) = 
          fix (loopAux (mat.LC (l,nonlinear))) (sqcup(dfrI(vars),MR))
end
    
end; (* structure sop_bar *)


(*
 * THE ANALYSIS ALGORITHM
 *)


(* ANALYSIS OF EXPRESSIONS - in two versions *)

(* the purpose of these functions is to abstract an expression into a 
   single column matrix, sorted! *)

(*Input to analysis functor*)
signature ANALYSIS_PARMS =
  sig
  val nonlinear_Dvalue: D.t;
  val name: string
  end;

functor analysis(analysis_kind: ANALYSIS_PARMS) = struct

(* abstract addition of 'columns' *)
local
 fun add' d = D.lub(D.One',d);
 fun add'' (i,d) = (i, add' d);
in
fun add([], ys) = map add'' ys
  | add(xs, []) = map add'' xs
  | add(xs as ((i,d)::xt), ys as ((i',d')::yt)) = 
       if i=i' then (i,D.sum(d,d')) :: add(xt,yt)
       else if i<i' then (i,add' d) :: add(xt,ys)
       else (i',add' d') :: add(xs,yt)
end;

(* utility functions: collect the variables in an Expr, or find the highest *)

local
 fun merge([],ys) = ys
   | merge(xs,[]) = xs
   | merge(xs as (x::xt), ys as (y::yt)) =
        if x=y then x::(merge(xt,yt))
        else if x<y then x::(merge(xt,ys))
        else y::(merge(xs,yt)) ;
        
fun highest_var_inE(Core.Var i) = i
  | highest_var_inE(Core.plus(e1, e2)) = Int.max(highest_var_inE e1, highest_var_inE e2)
  | highest_var_inE(Core.times(e1, e2))= Int.max(highest_var_inE e1, highest_var_inE e2)
  | highest_var_inE(Core.Zero) = 1;
  
in
fun vars(Core.Var i) = [i]
  | vars(Core.plus(e1, e2)) = merge(vars e1, vars e2)
  | vars(Core.times(e1, e2)) = merge(vars e1, vars e2)
  | vars(Core.Zero) = []

fun highest_var(Core.Skip) = 1
  | highest_var(Core.Asgn(j,e)) = Int.max(j, highest_var_inE e)
  | highest_var(Core.Seq(C1,C2)) = Int.max(highest_var C1, highest_var C2) 
  | highest_var(Core.Choice(C1,C2)) = Int.max(highest_var C1, highest_var C2)
  | highest_var(Core.Loop(l,C)) = Int.max(l, highest_var C);
end;
 
 
(* analyse an expression.  *)
fun analyseE (Core.Var i) = [(i,D.One)]
  | analyseE (Core.plus(e1, e2)) = add(analyseE e1, analyseE e2)
  | analyseE (e as (Core.times( _, _))) = 
           map (fn i => (i,analysis_kind.nonlinear_Dvalue)) (vars e)
  | analyseE(Core.Zero) = raise Fail "Zero assignment is unsupported."



(* main function: analyse a command *)


fun analyse(c) = 
let val vars = highest_var c;  
fun analyseC (Core.Skip) = sop_bar.dfrI(vars)
    
 |  analyseC (Core.Asgn(j,e)) = 
     let val col = 
              (List.map (fn (i,r) => (i,j,r)) (analyseE e));
          val m = mat.ins_in_I(vars,j,col)
     in
       sop_bar.dfr(m,mat.r(m))
     end
 
 |  analyseC (Core.Seq(C1,C2)) =
   sop_bar.prod(analyseC C1, analyseC C2)

 |  analyseC (Core.Choice(C1,C2)) =
   sop_bar.sqcup(analyseC C1, analyseC C2)
   
 |  analyseC (Core.Loop(l,C)) =
   sop_bar.loop(l,vars,analysis_kind.nonlinear_Dvalue,(analyseC C));
 in
   let val sop_bar.dfr(M,R) = analyseC c ;
       fun prt_ints [] = "\n"
         | prt_ints (i::rest) = 
           (Int.toString i) ^ (if rest<>[] then ", "^(prt_ints rest) else "\n");
       val (nonbounded, bounded) = mat.classify(M,vars)
   in (print ("VARS: "^(Int.toString vars)^"\n");
       print  (analysis_kind.name^": "); print (prt_ints bounded);
       print ("NON-"^analysis_kind.name^": "); print (prt_ints nonbounded);
 	   sop_bar.dfr (M, R))
	   (*
	   (mat.lstPrt(M), R))
*)
   end
 end;

end; (* analysis *)

structure Pol = analysis(struct val nonlinear_Dvalue = D.Two;
                                val name = "POLYNOMIAL" end);
structure Lin = analysis(struct val nonlinear_Dvalue = D.Three
								val name = "LINEAR" end);





